Bob is blue. Bob is cold. Bob is furry. Bob is kind. Bob is red. Bob is round. Bob is young. If something is round and not furry then it is blue. If something is young and not round then it is not cold. If something is blue and not furry then it is red. If something is kind then it is young. Furry things are young. All young things are kind.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
If something is round and not furry then it is blue.
((("something" "is" "round" "+") ("something" "is" "furry" "~")) -> ("something" "is" "blue" "+"))
If something is young and not round then it is not cold.
((("something" "is" "young" "+") ("something" "is" "round" "~")) -> ("something" "is" "cold" "-"))
If something is blue and not furry then it is red.
((("something" "is" "blue" "+") ("something" "is" "furry" "~")) -> ("something" "is" "red" "+"))
If something is kind then it is young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
All young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
Bob is cold.
True
1
proof
[(triple2)]
("Bob" "is" "cold" "+")
triple2
Bob is not young.
False
1
inv-proof
[(triple7 OR ((triple3) -> rule5) OR ((triple4) -> rule4))]
("Bob" "is" "young" "-")
triple7
((triple3) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple4) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2)] Bob is furry.[(triple3)] Bob is kind.[(triple4 OR ((triple7) -> rule6) OR ((((triple3) -> rule5)) -> rule6))] Bob is red.[(triple5)] Bob is round.[(triple6)] Bob is young.[(triple7 OR ((triple3) -> rule5) OR ((triple4) -> rule4))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
((triple7) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple3) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple4) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1