Bob is cold. Bob is kind. Bob is quiet. Bob is rough. Bob is white. Harry is cold. Harry is furry. Harry is kind. Harry is quiet. Harry is rough. Harry is round. Harry is white. Quiet people are furry. If Bob is white then Bob is cold. If someone is round and rough then they are white. If someone is quiet then they are white. Round people are kind. Quiet, round people are rough.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
Quiet people are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If Bob is white then Bob is cold.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "cold" "+"))
If someone is round and rough then they are white.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If someone is quiet then they are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Round people are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
Quiet, round people are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Harry is furry.
True
1
proof
[(triple7 OR ((triple9) -> rule1))]
("Harry" "is" "furry" "+")
triple7
((triple9) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not quiet.
False
1
inv-proof
[(triple9)]
("Harry" "is" "quiet" "-")
triple9
@0: Bob is cold.[(triple1 OR ((triple5) -> rule2) OR ((((triple3) -> rule4)) -> rule2))] Bob is kind.[(triple2)] Bob is quiet.[(triple3)] Bob is rough.[(triple4)] Bob is white.[(triple5 OR ((triple3) -> rule4))] Harry is cold.[(triple6)] Harry is furry.[(triple7 OR ((triple9) -> rule1))] Harry is kind.[(triple8 OR ((triple11) -> rule5))] Harry is quiet.[(triple9)] Harry is rough.[(triple10 OR ((triple9 triple11) -> rule6))] Harry is round.[(triple11)] Harry is white.[(triple12 OR ((triple9) -> rule4) OR ((triple11 triple10) -> rule3) OR ((triple11 ((triple9 triple11) -> rule6)) -> rule3))] @1: Bob is furry.[(((triple3) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple5) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
((triple3) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
((triple9) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple8
((triple11) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple10
((triple9 triple11) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
((triple9) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple11 triple10) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple11 ((triple9 triple11) -> (rule6 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((triple3) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1