Bob is not big. Bob is blue. Bob is cold. Bob is kind. Bob is nice. Bob is red. Harry is big. Harry is blue. Harry is not cold. Harry is nice. Harry is red. Harry is young. If something is nice and not kind then it is not red. If something is cold then it is not young. All cold, red things are nice. Big, kind things are nice. Cold, red things are nice. If Bob is red then Bob is cold.
Bob is not big.
("Bob" "is" "big" "-")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is nice and not kind then it is not red.
((("something" "is" "nice" "+") ("something" "is" "kind" "~")) -> ("something" "is" "red" "-"))
If something is cold then it is not young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "-"))
All cold, red things are nice.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Big, kind things are nice.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Cold, red things are nice.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If Bob is red then Bob is cold.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "cold" "+"))
Bob is not big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Bob is not kind.
False
1
inv-proof
[(triple4)]
("Bob" "is" "kind" "-")
triple4
@0: Bob is blue.[(triple2)] Bob is cold.[(triple3 OR ((triple6) -> rule6))] Bob is kind.[(triple4)] Bob is nice.[(triple5 OR ((triple3 triple6) -> rule3) OR ((triple3 triple6) -> rule5) OR ((((triple6) -> rule6) triple6) -> rule3) OR ((((triple6) -> rule6) triple6) -> rule5))] Bob is not big.[(triple1)] Bob is red.[(triple6)] Harry is big.[(triple7)] Harry is blue.[(triple8)] Harry is nice.[(triple10)] Harry is not cold.[(triple9)] Harry is red.[(triple11)] Harry is young.[(triple12)] @1: Bob is not young.[(((triple3) -> rule2) OR ((((triple6) -> rule6)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
((triple6) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Bob is nice.
("Bob" "is" "nice" "+")
triple5
((triple3 triple6) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple3 triple6) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple6) -> (rule6 % int2)) triple6) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple6) -> (rule6 % int2)) triple6) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not big.
("Bob" "is" "big" "-")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is not cold.
("Harry" "is" "cold" "-")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Bob is not young.
("Bob" "is" "young" "-")
((triple3) -> (rule2 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2