Bob is big. Bob is furry. Bob is green. Bob is nice. Bob is red. Bob is white. Harry is furry. Harry is green. Harry is nice. Harry is red. Harry is white. Harry is young. All young people are big. All red, furry people are white. All white people are green.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
All young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
All red, furry people are white.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
All white people are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
Harry is nice.
True
1
proof
[(triple9)]
("Harry" "is" "nice" "+")
triple9
Harry is not green.
False
1
inv-proof
[(triple8 OR ((triple11) -> rule3) OR ((((triple10 triple7) -> rule2)) -> rule3))]
("Harry" "is" "green" "-")
triple8
((triple11) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple10 triple7) -> (rule2 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
@0: Bob is big.[(triple1)] Bob is furry.[(triple2)] Bob is green.[(triple3 OR ((triple6) -> rule3) OR ((((triple5 triple2) -> rule2)) -> rule3))] Bob is nice.[(triple4)] Bob is red.[(triple5)] Bob is white.[(triple6 OR ((triple5 triple2) -> rule2))] Harry is furry.[(triple7)] Harry is green.[(triple8 OR ((triple11) -> rule3) OR ((((triple10 triple7) -> rule2)) -> rule3))] Harry is nice.[(triple9)] Harry is red.[(triple10)] Harry is white.[(triple11 OR ((triple10 triple7) -> rule2))] Harry is young.[(triple12)] @1: Harry is big.[(((triple12) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
((triple6) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple5 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
((triple5 triple2) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
((triple11) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple10 triple7) -> (rule2 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple10
Harry is white.
("Harry" "is" "white" "+")
triple11
((triple10 triple7) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple12
Harry is big.
("Harry" "is" "big" "+")
((triple12) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1