Bob is cold. Bob is green. Bob is nice. Bob is rough. Bob is not round. Bob is not white. Bob is young. Dave is cold. Dave is green. Dave is nice. Dave is not rough. Dave is white. All white people are round. If someone is round then they are young. All rough people are young. White, rough people are cold. If Bob is green then Bob is not white. If Dave is not cold and Dave is not round then Dave is not young.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is not round.
("Bob" "is" "round" "-")
Bob is not white.
("Bob" "is" "white" "-")
Bob is young.
("Bob" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is white.
("Dave" "is" "white" "+")
All white people are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
All rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
White, rough people are cold.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If Bob is green then Bob is not white.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "white" "-"))
If Dave is not cold and Dave is not round then Dave is not young.
((("Dave" "is" "cold" "~") ("Dave" "is" "round" "~")) -> ("Dave" "is" "young" "-"))
Dave is cold.
True
1
proof
[(triple8)]
("Dave" "is" "cold" "+")
triple8
Dave is not green.
False
1
inv-proof
[(triple9)]
("Dave" "is" "green" "-")
triple9
Dave is round.
True
2
proof
[(((triple12) -> rule1))]
("Dave" "is" "round" "+")
((triple12) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple12) -> rule1))]
("Dave" "is" "round" "-")
((triple12) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
True
3
proof
[(((((triple12) -> rule1)) -> rule2))]
("Dave" "is" "young" "+")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not young.
False
3
inv-proof
[(((((triple12) -> rule1)) -> rule2))]
("Dave" "is" "young" "-")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
@0: Bob is cold.[(triple1)] Bob is green.[(triple2)] Bob is nice.[(triple3)] Bob is not round.[(triple5)] Bob is not white.[(triple6 OR ((triple2) -> rule5))] Bob is rough.[(triple4)] Bob is young.[(triple7 OR ((triple4) -> rule3))] Dave is cold.[(triple8)] Dave is green.[(triple9)] Dave is nice.[(triple10)] Dave is not rough.[(triple11)] Dave is white.[(triple12)] @1: Dave is round.[(((triple12) -> rule1))] @2: Dave is young.[(((((triple12) -> rule1)) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is not round.
("Bob" "is" "round" "-")
triple5
Bob is not white.
("Bob" "is" "white" "-")
triple6
((triple2) -> (rule5 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple4) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple8
Dave is green.
("Dave" "is" "green" "+")
triple9
Dave is nice.
("Dave" "is" "nice" "+")
triple10
Dave is not rough.
("Dave" "is" "rough" "-")
triple11
Dave is white.
("Dave" "is" "white" "+")
triple12
Dave is round.
("Dave" "is" "round" "+")
((triple12) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2