Bob is big. Bob is cold. Bob is furry. Bob is quiet. Bob is round. Harry is not big. Harry is cold. Harry is furry. Harry is quiet. Harry is rough. Harry is round. Harry is young. All cold people are young. Furry people are quiet.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
All cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
Furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
Harry is cold.
True
1
proof
[(triple7)]
("Harry" "is" "cold" "+")
triple7
Harry is not cold.
False
1
inv-proof
[(triple7)]
("Harry" "is" "cold" "-")
triple7
Bob is young.
True
2
proof
[(((triple2) -> rule1))]
("Bob" "is" "young" "+")
((triple2) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "young" "-")
((triple2) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
@0: Bob is big.[(triple1)] Bob is cold.[(triple2)] Bob is furry.[(triple3)] Bob is quiet.[(triple4 OR ((triple3) -> rule2))] Bob is round.[(triple5)] Harry is cold.[(triple7)] Harry is furry.[(triple8)] Harry is not big.[(triple6)] Harry is quiet.[(triple9 OR ((triple8) -> rule2))] Harry is rough.[(triple10)] Harry is round.[(triple11)] Harry is young.[(triple12 OR ((triple7) -> rule1))] @1: Bob is young.[(((triple2) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple3) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
triple8
Harry is not big.
("Harry" "is" "big" "-")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
((triple8) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Harry is round.
("Harry" "is" "round" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
((triple7) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple2) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1