Bob is big. Bob is blue. Bob is furry. Bob is kind. Bob is nice. Bob is red. Bob is smart. Dave is big. Dave is furry. Dave is kind. Dave is red. Dave is smart. If Bob is big then Bob is smart. Big, kind things are nice.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If Bob is big then Bob is smart.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "smart" "+"))
Big, kind things are nice.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Dave is big.
True
1
proof
[(triple8)]
("Dave" "is" "big" "+")
triple8
Bob is not furry.
False
1
inv-proof
[(triple3)]
("Bob" "is" "furry" "-")
triple3
Dave is nice.
True
3
proof
[(((triple8 triple10) -> rule2))]
("Dave" "is" "nice" "+")
((triple8 triple10) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
3
inv-proof
[(((triple8 triple10) -> rule2))]
("Dave" "is" "nice" "-")
((triple8 triple10) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is furry.[(triple3)] Bob is kind.[(triple4)] Bob is nice.[(triple5 OR ((triple1 triple4) -> rule2))] Bob is red.[(triple6)] Bob is smart.[(triple7 OR ((triple1) -> rule1))] Dave is big.[(triple8)] Dave is furry.[(triple9)] Dave is kind.[(triple10)] Dave is red.[(triple11)] Dave is smart.[(triple12)] @1: Dave is nice.[(((triple8 triple10) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Bob is nice.
("Bob" "is" "nice" "+")
triple5
((triple1 triple4) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple6
Bob is smart.
("Bob" "is" "smart" "+")
triple7
((triple1) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is furry.
("Dave" "is" "furry" "+")
triple9
Dave is kind.
("Dave" "is" "kind" "+")
triple10
Dave is red.
("Dave" "is" "red" "+")
triple11
Dave is smart.
("Dave" "is" "smart" "+")
triple12
Dave is nice.
("Dave" "is" "nice" "+")
((triple8 triple10) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1