Bob is cold. Bob is furry. Bob is kind. Bob is red. Bob is rough. Bob is young. Dave is cold. Dave is kind. Dave is red. Dave is rough. If someone is cold then they are round. If Dave is round and Dave is kind then Dave is furry. If someone is round and kind then they are young.
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 rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
If someone is cold then they are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If Dave is round and Dave is kind then Dave is furry.
((("Dave" "is" "round" "+") ("Dave" "is" "kind" "+")) -> ("Dave" "is" "furry" "+"))
If someone is round and kind then they are young.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
Dave is rough.
True
1
proof
[(triple10)]
("Dave" "is" "rough" "+")
triple10
Dave is not red.
False
1
inv-proof
[(triple9)]
("Dave" "is" "red" "-")
triple9
Bob is round.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "round" "+")
((triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple7) -> rule1))]
("Dave" "is" "round" "-")
((triple7) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
True
4
proof
[(((((triple7) -> rule1) triple8) -> rule3))]
("Dave" "is" "young" "+")
((((triple7) -> (rule1 % int2)) triple8) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not furry.
False
4
inv-proof
[(((((triple7) -> rule1) triple8) -> rule2))]
("Dave" "is" "furry" "-")
((((triple7) -> (rule1 % int2)) triple8) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
@0: Bob is cold.[(triple1)] Bob is furry.[(triple2)] Bob is kind.[(triple3)] Bob is red.[(triple4)] Bob is rough.[(triple5)] Bob is young.[(triple6 OR ((((triple1) -> rule1) triple3) -> rule3))] Dave is cold.[(triple7)] Dave is kind.[(triple8)] Dave is red.[(triple9)] Dave is rough.[(triple10)] @1: Bob is round.[(((triple1) -> rule1))] Dave is round.[(((triple7) -> rule1))] @2: Dave is furry.[(((((triple7) -> rule1) triple8) -> rule2))] Dave is young.[(((((triple7) -> rule1) triple8) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is young.
("Bob" "is" "young" "+")
triple6
((((triple1) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
triple7
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple9
Dave is rough.
("Dave" "is" "rough" "+")
triple10
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple7) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple7) -> (rule1 % int2)) triple8) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((triple7) -> (rule1 % int2)) triple8) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2