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