Bob is big. Bob is blue. Bob is furry. Bob is quiet. Bob is rough. Bob is round. Bob is smart. Harry is big. Harry is blue. Harry is furry. Harry is quiet. Harry is rough. If someone is round and blue then they are big. If Harry is quiet and Harry is round then Harry is blue. Smart, blue people are round. If Harry is blue then Harry is smart. If Harry is furry and Harry is blue then Harry is rough. All round, rough people are quiet. All furry, smart people are big. If Harry is rough and Harry is round then Harry is furry.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is round and blue then they are big.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
If Harry is quiet and Harry is round then Harry is blue.
((("Harry" "is" "quiet" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "blue" "+"))
Smart, blue people are round.
((("someone" "is" "smart" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If Harry is blue then Harry is smart.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "smart" "+"))
If Harry is furry and Harry is blue then Harry is rough.
((("Harry" "is" "furry" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "rough" "+"))
All round, rough people are quiet.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
All furry, smart people are big.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If Harry is rough and Harry is round then Harry is furry.
((("Harry" "is" "rough" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "furry" "+"))
Bob is rough.
True
1
proof
[(triple5)]
("Bob" "is" "rough" "+")
triple5
Harry is not furry.
False
1
inv-proof
[(triple10 OR ((triple12 ((((triple9) -> rule4) triple9) -> rule3)) -> rule8))]
("Harry" "is" "furry" "-")
triple10
((triple12 ((((triple9) -> (rule4 % int3)) triple9) -> (rule3 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is smart.
True
2
proof
[(((triple9) -> rule4))]
("Harry" "is" "smart" "+")
((triple9) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple9) -> rule4))]
("Harry" "is" "smart" "-")
((triple9) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
True
4
proof
[(((((triple9) -> rule4) triple9) -> rule3))]
("Harry" "is" "round" "+")
((((triple9) -> (rule4 % int2)) triple9) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not round.
False
4
inv-proof
[(((((triple9) -> rule4) triple9) -> rule3))]
("Harry" "is" "round" "-")
((((triple9) -> (rule4 % int2)) triple9) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
@0: Bob is big.[(triple1 OR ((triple3 triple7) -> rule7) OR ((triple6 triple2) -> rule1) OR ((((triple7 triple2) -> rule3) triple2) -> rule1))] Bob is blue.[(triple2)] Bob is furry.[(triple3)] Bob is quiet.[(triple4 OR ((triple6 triple5) -> rule6) OR ((((triple7 triple2) -> rule3) triple5) -> rule6))] Bob is rough.[(triple5)] Bob is round.[(triple6 OR ((triple7 triple2) -> rule3))] Bob is smart.[(triple7)] Harry is big.[(triple8 OR ((triple10 ((triple9) -> rule4)) -> rule7) OR ((((((triple9) -> rule4) triple9) -> rule3) triple9) -> rule1) OR ((((triple12 ((((triple9) -> rule4) triple9) -> rule3)) -> rule8) ((triple9) -> rule4)) -> rule7))] Harry is blue.[(triple9)] Harry is furry.[(triple10 OR ((triple12 ((((triple9) -> rule4) triple9) -> rule3)) -> rule8))] Harry is quiet.[(triple11 OR ((((((triple9) -> rule4) triple9) -> rule3) triple12) -> rule6) OR ((((((triple9) -> rule4) triple9) -> rule3) ((triple10 triple9) -> rule5)) -> rule6))] Harry is rough.[(triple12 OR ((triple10 triple9) -> rule5))] @1: Harry is smart.[(((triple9) -> rule4))] @2: Harry is round.[(((((triple9) -> rule4) triple9) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3 triple7) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple6 triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple7 triple2) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple6 triple5) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple7 triple2) -> (rule3 % int2)) triple5) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple7 triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
((triple10 ((triple9) -> (rule4 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((((triple9) -> (rule4 % int3)) triple9) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((triple12 ((((triple9) -> (rule4 % int4)) triple9) -> (rule3 % int3))) -> (rule8 % int2)) ((triple9) -> (rule4 % int4))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
((triple12 ((((triple9) -> (rule4 % int3)) triple9) -> (rule3 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
((((((triple9) -> (rule4 % int3)) triple9) -> (rule3 % int2)) triple12) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((triple9) -> (rule4 % int4)) triple9) -> (rule3 % int3)) ((triple10 triple9) -> (rule5 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
triple12
((triple10 triple9) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple9) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple9) -> (rule4 % int2)) triple9) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2