Bob is cold. Bob is furry. Bob is nice. Bob is quiet. Bob is round. Bob is white. Bob is young. Charlie is cold. Charlie is furry. Charlie is nice. Charlie is quiet. Charlie is round. Charlie is white. Charlie is young. If Bob is round then Bob is young.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If Bob is round then Bob is young.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "young" "+"))
Charlie is young.
True
1
proof
[(triple14)]
("Charlie" "is" "young" "+")
triple14
Bob is not cold.
False
1
inv-proof
[(triple1)]
("Bob" "is" "cold" "-")
triple1
@0: Bob is cold.[(triple1)] Bob is furry.[(triple2)] Bob is nice.[(triple3)] Bob is quiet.[(triple4)] Bob is round.[(triple5)] Bob is white.[(triple6)] Bob is young.[(triple7 OR ((triple5) -> rule1))] Charlie is cold.[(triple8)] Charlie is furry.[(triple9)] Charlie is nice.[(triple10)] Charlie is quiet.[(triple11)] Charlie is round.[(triple12)] Charlie is white.[(triple13)] Charlie is young.[(triple14)]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple5) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple8
Charlie is furry.
("Charlie" "is" "furry" "+")
triple9
Charlie is nice.
("Charlie" "is" "nice" "+")
triple10
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple11
Charlie is round.
("Charlie" "is" "round" "+")
triple12
Charlie is white.
("Charlie" "is" "white" "+")
triple13
Charlie is young.
("Charlie" "is" "young" "+")
triple14